Missed or omitted requirements in system development means a large correction cost incurred by a return for rework from subsequent steps, and the need to detect missed or omitted requirements early is therefore widely known. In conventional detection of missed or omitted requirements, a person visually checks for a problem in a document that describes requirements by looking over prepared check items. In the case where there are a source document and a response document such as a request for proposal (RFP) and a proposal in response to the RFP, or a proposal and specifications in response to the proposal, the person also visually checks whether or not the response document contains points that correspond to individual matters written in the source document. However, checking a voluminous document that contains duplicate statements is costly (in terms of labor cost and time), and has a problem in that an overlook may occur in the manual check.
To cope with this, a technology for performing formal verification by modeling a subject is disclosed in Patent Literature 1, with which whether or not there is a problem can be verified about a described matter. However, describing and deciphering are skills to be learned by a user over time. Another problem is that the verification is not precise if the conversion from a document which is a natural language to a formal description is incorrect.
Technologies for assisting formal verification are disclosed in Patent Literature 2, Patent Literature 3, Patent Literature 4, and others, but do not solve the problem of the necessity of learning in using the formal verification. A general document, too, is reviewed manually for contradictions and ambiguities in the document and, in the case where a new document is created from a source document, for a matter that is written in the source document and missed or omitted in the new document, and similarly has the problem of cost (labor cost and time) and an overlook in the manual check.